A, B:Realizer. R-Feasible(A)  R-Feasible(B)  A || B  [[A]] || [[B]] 

latex

Definitions	x:A. B(x), P  Q, AB, t  T, if b t else f fi, true, P  Q, Prop, P & Q, P  Q, false, T, True, A, False, A & B, , , Unit, S  T,
Lemmas	R-compat-Dsys, ifthenelse wf, le int wf, R-size wf, nat plus wf, nat wf, nat plus inc, bool wf, iff transitivity, assert wf, le wf, eqtt to assert, assert of le int, lt int wf, bnot wf, eqff to assert, squash wf, true wf, bnot of le int, assert of lt int, R-compat wf, R-Feasible wf, es realizer wf